proposition: Theorem mult_plus_distr_l (alpha beta gamma: E0) : alpha * (beta + gamma) = alpha * beta + alpha * gamma.
proof: Proof. destruct alpha, beta, gamma; apply E0_eq_intro; cbn; now apply T1.mult_plus_distr_l. 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)