proposition: Lemma int_pos_sub_add (a b c : Pos) : int_pos_sub (a + b)%pos c = pos a + int_pos_sub b c.
proof: Proof. revert c b a. induction c as [|c ch] using pos_peano_ind. { intros b a. change (int_pred (pos a + pos b) = pos a + (int_pred (pos b))). apply int_pred_add_r. } intros b a. rewrite <- int_pred_pos_sub_r. rewrite ch. rewrite <- int_pred_pos_sub_r. apply int_pred_add_r. Defined.
imports: Basics Spaces.Pos Spaces.Int.Core