n m p : (n + m) * p = n * p + m * p. Proof. induction p; destruct n, m; cbn; trivial; try f_ap; try apply pos_mul_add_distr_r; try apply binint_pos_sub_mul_neg; try apply binint_pos_sub_mul_pos; apply binint_mul_0_r. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.