proposition: Lemma ltb_ind (P: nat -> nat -> Prop) (H0: forall n, P (S n) 0) (HS: forall n i, P n i -> P (S n) (S i)): forall n i, i<n -> P n i.
proof: Proof. induction n; intros i Hi. destruct i; discriminate. destruct i. apply H0. now apply HS, IHn. Qed.
imports: List PeanoNat common comparisons