proposition: Lemma FindPointInSubdivisionSmallest : forall (Pn : nat -> nat) (Pinc : forall k, lt (Pn k) (Pn (S k))) (Pzero : Pn O = O) (n i : nat), le (Pn i) n -> le i (proj1_sig (FindPointInSubdivision Pn n Pinc Pzero)).
proof: Proof. induction i. - intros. apply Nat.le_0_l. - intros. destruct (FindPointInSubdivision Pn n Pinc Pzero) as [r rmaj]. simpl in IHi. simpl. assert (i <= r)%nat. apply IHi. apply (Nat.le_trans _ (Pn (S i))). 2: apply H. specialize (Pinc i). apply le_S in Pinc. apply le_S_n in Pinc. apply Pinc. clear IHi. apply le_n_S in H0. apply Nat.le_succ_r in H0. destruct H0. apply H0. exfalso. inversion H0. subst i. apply Nat.le_ngt in H. destruct rmaj. contradiction. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits