proposition: Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l.
proof: Proof. induction 1 as [|a b c H0 H1 H2 H3]. - auto. - eapply Nat.le_trans; eauto. apply between_le in H2. transitivity (S a); auto. Qed.
imports: PeanoNat