Read Me

C'est sale pour l'instant, je refais plusieurs fois les memes preuves


La preuve de meme evaluation -> meme poly est dans projet1.v


(* SPOILER *)

Ca commence à 
(* TODO DEBUT EVAL *)

Il est interessant de regarder l'argument des generalize sur les evaluations.
(on peut voir comment il est créé dans Zax.v (les hypotheses chelou en bas))
p2equalq2 est surement interessant à checker. (bon ok j'y fais au moins deux fois la meme preuve...*)
Truc interessant: 
evaal_good: forall val, val n0 * evaluation val q2 = 0 -> q2 = Cst z est un lemme intéressant a regarder si mes souvenirs sont bons

Arguments utilisés : induction, new inductifs à la con, et 
(forall (x y z : Z), |x| > |y| -> x*z = y -> z = 0 et y = 0)

TODO regarder la preuve...

Le lemme s'appelle evaluation_equal