proposition: Lemma nat_double_rect : forall (P:nat->Type), P 0 -> P 1 -> (forall p, P p -> P (S (S p))) -> forall n:nat, P n.
proof: Proof. intros P H0 H1 HS. assert (X : forall n, (P n * P (S n)%type)). - induction n as [| p IHp]; [auto | destruct IHp;auto]. - intro n; now destruct (X n). Qed.
imports: Arith Lia