proposition: Fact scal_times k x y : scal k (x⊗y) = x⊗scal k y.
proof: Proof. Proof using M_sum M_times sum_cancel distr_l. destruct M_sum as [ S1 S2 S3 ]. destruct M_times as [ T1 T2 T3 ]. induction k as [ | k IHk ]. + rewrite mscal_0, mscal_0, times_zero_r; auto. + rewrite mscal_S, mscal_S, IHk, distr_l; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)