proposition: Lemma mul_add_distr_r n m p : (n + m) * p = n * p + m * p.
proof: Proof. destruct p as [|p|p]. - now rewrite !mul_0_r. - apply mul_add_distr_pos. - apply opp_inj. rewrite opp_add_distr, <- !mul_opp_r. apply mul_add_distr_pos. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass