proposition: Lemma mult_plus_distr_l (a b c: t) : nf a -> nf b -> nf c -> a * (b + c) = a * b + a * c.
proof: Proof. intros Ha Hb Hc; apply eq_ref; rewrite !mult_ref, !plus_ref, T1.mult_plus_distr_l, !mult_ref; trivial. all: now apply nf_ref. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )