proposition: Lemma StartZeroInc : forall (un : nat -> nat), (forall n:nat, lt (un n) (un (S n))) -> (forall n:nat, lt (StartZero un n) (StartZero un (S n))).
proof: Proof. intros. destruct n. - simpl. destruct (un O) eqn:des. apply (Nat.le_lt_trans _ (un O)). apply Nat.le_0_l. apply H. apply le_n_S, Nat.le_0_l. - simpl. destruct (un O); apply H. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity