proposition: Lemma oplus_strict_mono_l (a b c: T1): T1nf a -> T1nf b -> T1nf c -> a < b -> a o+ c < b o+ c.
proof: Proof. rewrite /oplus => Ha Hb Hc; rewrite <- hlt_iff => Hab. apply oplus_strict_mono_l ; rewrite ?hnf_g2h ?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)