proposition: Lemma alpha_plus_zero alpha : alpha + E0zero = alpha.
proof: Proof. apply E0_eq_intro; simpl; now rewrite plus_zero_r. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)