proposition: Lemma E0compare_correct (alpha beta : E0) : CompSpec eq E0lt alpha beta (compare alpha beta).
proof: Proof. destruct alpha, beta; rewrite /compare; case (T1compare_correct cnf0 cnf1) => Hcomp. { subst; replace i0 with i. + rewrite /E0compare; cbn. replace (compare (g2h cnf1) (g2h cnf1)) with Datatypes.Eq => //. * by constructor. * by rewrite compare_refl. + apply eq_proofs_unicity_on; by destruct y, (T1nf cnf1) => //; [left | right] => //. } { rewrite /E0compare; cbn. replace (compare (g2h cnf0) (g2h cnf1)) with Datatypes.Lt. + constructor; rewrite /E0lt => //. + move: Hcomp; rewrite /compare T1lt_iff. case ; rewrite -compare_lt_iff => _ [Hcomp _]. symmetry; by rewrite compare_lt_iff. 1, 2: by apply /eqP. } rewrite /E0compare; cbn. replace (compare (g2h cnf0) (g2h cnf1)) with Datatypes.Gt. + constructor; rewrite /E0lt => //. + move: Hcomp; rewrite /compare T1lt_iff. case ; rewrite -compare_gt_iff => // _ [Hcomp _] //. all: by apply /eqP. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0) Coq(Relations Basics Wellfounded.Inverse_Image Wellfounded.Inclusion)