proposition: Theorem lt_ind_rel : (forall m, R 0 (S m)) -> (forall n m, n < m -> R n m -> R (S n) (S m)) -> forall n m, n < m -> R n m.
proof: Proof. intros Base Step n; induct n. - intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]]. rewrite H; apply Base. - intros n IH m H. elim H using lt_ind. + solve_proper. + apply Step; [| apply IH]; now apply lt_succ_diag_r. + intros k H1 H2. apply lt_succ_l in H1. auto. Qed.
imports: NAdd