proposition: Lemma oplus_lt_phi0 (a b c: T1): T1nf a -> T1nf b -> T1nf c -> a < c -> b < c -> phi0 a o+ phi0 b < phi0 c.
proof: Proof. move => Ha Hb Hc Hab Hbc; rewrite /oplus. replace (phi0 c) with (h2g (T1.phi0 (g2h c))); last first. by rewrite -g2h_phi0 ?h2g_g2hK. rewrite -hlt_iff !g2h_phi0. apply oplus_lt_phi0; 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)