proposition: Lemma R__S_I__S s: (R__S (I__S s)) = s.
proof: Proof. unfold I__S, R__S. destruct s. - specialize (Nat.even_spec (Nat.double n)) as [_ H]. rewrite H, Nat.double_twice, Nat.div2_double; eauto. eapply Nat.even_spec. unfold Nat.double. rewrite Nat.even_add. destruct (Nat.even n); reflexivity. - specialize (Nat.even_spec (Nat.double n)) as [_ H]. rewrite Nat.even_succ, <-Nat.negb_even. rewrite H; cbn [negb]. rewrite Nat.double_twice, Nat.div2_succ_double; eauto. eapply Nat.even_spec; unfold Nat.double; rewrite ?Nat.even_add; destruct (Nat.even n); reflexivity. Qed.
imports: FinFun Undecidability.HOU(std.decidable) Arith Lia Nat Arith.Div2