proposition: Lemma ind_0_1_SS : 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 H2. fix IH 1. intros [|[|n]] ; try assumption. apply H2, IH. Qed.
imports: Coq(Reals Psatz ssreflect)