n m p : binint_pos_sub n m * pos p = binint_pos_sub (n * p)%pos (m * p)%pos. Proof. rewrite binint_mul_comm. rewrite 2 (pos_mul_comm _ p). induction p. { rewrite 2 pos_mul_1_l. apply binint_mul_1_l. } { cbn. rewrite <- IHp. set (binint_pos_sub n m) as k. by destruct k. } cbn. rewrite binint_pos_sub_add. rewrite <- (binint_pos_sub_negation _ (x0 _)). rewrite binint_pos_sub_add. rewrite binint_negation_add_distr. rewrite binint_pos_sub_negation. rewrite binint_add_assoc. cbn. rewrite <- IHp. set (binint_pos_sub n m) as k. by destruct k. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.