proposition: Lemma int_pred_double_int_pos_sub a b : int_pred_double (int_pos_sub (pos_succ a) b) = int_succ_double (int_pos_sub a b).
proof: Proof. revert a b. induction a; induction b; trivial. + by destruct b. + by destruct b. + cbn; by destruct (int_pos_sub a b). + cbn; by destruct (int_pos_sub a b). + cbn; apply ap. by rewrite pos_pred_double_succ. + cbn. rewrite <- IHa. by destruct (int_pos_sub (pos_succ a) b). + cbn. rewrite IHa. by destruct (int_pos_sub a b). Defined.
imports: Basics Spaces.Pos Spaces.Int.Core