proposition: Lemma mul_succ_l n m : succ n * m = n * m + m.
proof: Proof. unfold succ. now rewrite mul_add_distr_r, mul_1_l. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass