proposition: Lemma oplus_lt1 (a b:T1): T1nf a -> T1nf b -> zero < a -> b < b o+ a.
proof: Proof. move => Ha Hb Hlt; rewrite /oplus. replace b with (h2g (g2h b)) at 1 ; last first. by (rewrite h2g_g2hK). rewrite -hlt_iff; apply oplus_lt1 => //; rewrite ?hnf_g2h //. rewrite hlt_iff ?h2g_g2hK => //. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic) hydras(T1 E0 Hessenberg) gaia_hydras(T1Bridge)