proposition: Lemma ordered_transit : forall (xn : nat -> nat) (last : nat), (forall n:nat, S n <= last -> xn n < xn (S n))%nat -> (forall n p:nat, lt n p -> p <= last -> (xn n < xn p))%nat.
proof: Proof. induction p. - intros. exfalso. inversion H0. - intros. apply Nat.le_succ_r in H0. destruct H0. apply (Nat.lt_trans _ (xn p)). apply IHp. exact H0. apply (Nat.le_trans _ (S p)). apply le_S, Nat.le_refl. exact H1. apply H. exact H1. inversion H0. subst n. apply H. exact H1. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont