proposition: Lemma compare_ref (x y: hT1) : match T1.compare_T1 x y with | Datatypes.Lt => T1lt (h2g x) (h2g y) | Datatypes.Eq => h2g x = h2g y | Datatypes.Gt => T1lt (h2g y) (h2g x) end.
proof: Proof. move: y; elim: x => [|x1 IHx1 n x2 IHx2]; case => //= y1 n0 y2. case H: (Epsilon0.T1.compare_T1 x1 y1). - move: (IHx1 y1); rewrite H => {}IHx1. case H0: (PeanoNat.Nat.compare n n0). + have ->: (n = n0) by apply: Compare_dec.nat_compare_eq. case H1: (Epsilon0.T1.compare_T1 x2 y2). * rewrite IHx1; congr cons. move: (IHx2 y2); rewrite H1 => {}IHx2. case (h2g x1 < h2g y1); [trivial|]; by []. rewrite IHx1 eqxx /= eqxx ltnn. move: (IHx2 y2); rewrite H1 => {}IHx2; by rewrite T1ltnn. rewrite -IHx1 T1ltnn eqxx ltnn eqxx. move: (IHx2 y2); by rewrite H1. + rewrite IHx1 T1ltnn eqxx. have {}H0 : (n < n0)%coq_nat by apply: Compare_dec.nat_compare_Lt_lt. by move/ltP: H0 =>->. + rewrite IHx1 T1ltnn eqxx. apply Compare_dec.nat_compare_Gt_gt in H0. by move/ltP: H0 => ->. all: move: (IHx1 y1); by rewrite H => ->. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)