proposition: Lemma oplus_nf (a b : T1) : T1nf a -> T1nf b -> T1nf (a o+ b).
proof: Proof. rewrite /oplus -?nf_ref => Ha Hb; apply oplus_nf; by rewrite hnf_g2h. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic) hydras(T1 E0 Hessenberg) gaia_hydras(T1Bridge)