proposition: Theorem next_nat_closure_is_le : forall n m, (n <= m) <-> ((clos_refl_trans next_nat) n m).
proof: Proof. intros n m. split. - intro H. induction H. + apply rt_refl. + apply rt_trans with m. apply IHle. apply rt_step. apply nn. - intro H. induction H. + inversion H. apply le_S. apply le_n. + apply le_n. + apply le_trans with y. apply IHclos_refl_trans1. apply IHclos_refl_trans2. Qed.
imports: IndProp