proposition: Lemma T1compare_correct (a b: T1): CompSpec eq T1lt a b (compare a b).
proof: Proof. rewrite /compare /T1compare. case (T1.compare_correct (g2h a) (g2h b)). rewrite g2h_eqE => H; subst; by constructor. all: constructor; move:H; by rewrite lt_ref !h2g_g2hK . Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0) Coq(Relations Basics Wellfounded.Inverse_Image Wellfounded.Inclusion)