proposition: Lemma plus_ref : refines2 T1.T1add T1add.
proof: Proof. move => x; elim: x => [|x1 IHx1 n x2 IHx2]; case => //= y1 n0 y2. case Hx1y1: (Epsilon0.T1.compare_T1 x1 y1); move: (compare_ref x1 y1); rewrite Hx1y1 => H. - rewrite /Comparable.compare H T1ltnn /=. by rewrite Hx1y1 -H /=. - by rewrite /Comparable.compare H Hx1y1. - replace (h2g x1 < h2g y1) with false; last first. + by apply T1lt_anti in H. + rewrite /Comparable.compare H /= Hx1y1. change (cons (h2g y1) n0 (h2g y2)) with (h2g (T1.cons y1 n0 y2)); by rewrite IHx2. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)