(a b c : Pos) : binint_pos_sub (a + b)%pos c = pos a + binint_pos_sub b c. Proof. revert c b a. induction c as [|c ch] using pos_peano_ind. { intros b a. change (binint_pred (pos a + pos b) = pos a + (binint_pred (pos b))). apply binint_pred_add_r. } intros b a. rewrite <- binint_pred_pos_sub_r. rewrite ch. rewrite <- binint_pred_pos_sub_r. apply binint_pred_add_r. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.