proposition: Fact times_zero_l x : z ⊗ x = z.
proof: Proof. Proof using M_sum M_times sum_cancel distr_r. destruct M_sum as [ S1 S2 S3 ]. destruct M_times as [ T1 T2 T3 ]. apply sum_cancel with (z⊗x). rewrite S2, <- distr_r, S1; trivial. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)