proposition: Lemma evenSuccessor : forall n:nat, Nat.even (S n) = negb (Nat.even n).
proof: Proof. induction n. reflexivity. rewrite IHn. simpl. destruct (Nat.even n); reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase