proposition: Lemma oplus0b: left_id zero oplus.
proof: Proof. rewrite /oplus; case => // /= ? ? ?; by rewrite !h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic) hydras(T1 E0 Hessenberg) gaia_hydras(T1Bridge)