proposition: Lemma oplusA (a b c: T1) : T1nf a -> T1nf b -> T1nf c -> a o+ (b o+ c) = a o+ b o+ c.
proof: Proof. move => ? ? ?; by rewrite /oplus !g2h_h2gK oplus_assoc ?hnf_g2h. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic) hydras(T1 E0 Hessenberg) gaia_hydras(T1Bridge)