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