proposition: Lemma int_mul_add_distr_r n m p : (n + m) * p = n * p + m * p.
proof: Proof. induction p; destruct n, m; cbn; trivial; try f_ap; try apply pos_mul_add_distr_r; try apply int_pos_sub_mul_neg; try apply int_pos_sub_mul_pos; apply int_mul_0_r. Defined.
imports: Basics Spaces.Pos Spaces.Int.Core