(* Ad-hoc induction *) Fixpoint mod2 (n:nat) {struct n} : nat := match n with | O => O | (S O) => 1 | (S (S p)) => (mod2 p) end. Lemma mod_01 : forall n:nat, mod2 n =O \/ mod2 n=1. intros n ; elim n. left;trivial. intros n0 ; elim n0. intros H. right; trivial. intros n1 H1 H2. simpl. Abort. (* ??? *) Lemma mod_01 : forall n:nat, mod2 n =O \/ mod2 n=1. cut (forall n:nat,(((mod2 n=O)\/(mod2 n =1)) /\ ((mod2 (S n)=O)\/(mod2 (S n)=1)))). intros H n. elim (H n). intros H1 H2. apply H1. intros n ; elim n. split. left;trivial. right;trivial. intros n0 IH. elim IH; intros IH1 IH2. split. apply IH2. simpl. apply IH1. Qed. Reset mod_01. Functional Scheme mod_ind := Induction for mod2. Lemma mod_01 : forall n:nat, mod2 n =O \/ mod2 n=1. intros n ; elim n using mod_ind. intros; left; trivial. intros; right; trivial. intros n0 n1 Hn0n1 p Hn1p IH. simpl. apply IH. Qed.