proposition: Lemma compare_h2g (a beta: hT1) : compare (h2g a) (h2g beta) =compare a beta .
proof: Proof. rewrite -(g2h_h2gK a) -(g2h_h2gK beta). by rewrite compare_g2h !g2h_h2gK. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0) Coq(Relations Basics Wellfounded.Inverse_Image Wellfounded.Inclusion)