proposition: Theorem mul_succ_l : forall n m, (S n) * m == n * m + m.
proof: Proof. intros n m. zify. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l. now rewrite Z.mul_add_distr_r, Z.mul_1_l. Qed.
imports: NZAxioms ZArith Zpow_facts DoubleType CyclicAxioms Lia