proposition: Theorem le_ind_rel : (forall m, R 0 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; apply Base. } intros n IH m H. elim H using le_ind. - solve_proper. - apply Step; [| apply IH]; now apply eq_le_incl. - intros k H1 H2. apply le_succ_l in H1. apply lt_le_incl in H1. auto. Qed.
imports: NAdd