proposition: Lemma int_pos_sub_succ_succ a b : int_pos_sub (pos_succ a) (pos_succ b) = int_pos_sub a b.
proof: Proof. rewrite <- 2 pos_add_1_r. revert a b. induction a; induction b; trivial. 1: destruct b; trivial. { destruct b; trivial. cbn; apply ap. by rewrite pos_pred_double_succ. } 1: destruct a; trivial. 1: apply int_succ_double_int_pos_sub. { destruct a; trivial. cbn; apply ap, ap, pos_pred_double_succ. } 1: apply int_pred_double_int_pos_sub. cbn; apply ap. rewrite <- 2 pos_add_1_r. apply IHa. Defined.
imports: Basics Spaces.Pos Spaces.Int.Core