proposition: Lemma oplus_lt2 (a b: T1): T1nf a -> T1nf b -> zero < b -> a < b o+ a.
proof: Proof. move => Ha Hb HD; rewrite (oplusC Hb Ha); by apply oplus_lt1. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic) hydras(T1 E0 Hessenberg) gaia_hydras(T1Bridge)