proposition: Lemma mul_add_distr_pos (p:positive) n m : (n + m) * pos p = n * pos p + m * pos p.
proof: Proof. destruct n as [|n|n], m as [|m|m]; simpl; trivial. - now rewrite Pos.mul_add_distr_r. - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_r; case Pos.compare_spec; simpl; trivial; intros; now rewrite Pos.mul_sub_distr_r. - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_r; case Pos.compare_spec; simpl; trivial; intros; now rewrite Pos.mul_sub_distr_r. - now rewrite Pos.mul_add_distr_r. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass