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