proposition: Lemma E0g2h_plusE (a b: E0): E0_g2h (E0plus a b)= E0.E0add (E0_g2h a) (E0_g2h b).
proof: Proof. case: a ; case: b => a ? b ?; apply E0_eq_intro => /=; by rewrite g2h_plusE. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)