proposition: Lemma nat_double_ind : forall P : nat -> Prop, P 0 -> P 1 -> (forall n, P n -> P(S(S n))) -> forall n, P n.
proof: Proof. intros P H0 H1 Hind. apply nat_k_ind with 1. compute. split. exact H1. exact H0. exact Hind. Qed.
imports: PeanoNat Compare