proposition: Theorem lt_trans' : transitive lt.
proof: Proof. unfold lt. unfold transitive. intros n m o Hnm Hmo. induction Hmo as [| m' Hm'o]. Admitted. Theorem lt_trans'' : transitive lt. Proof. unfold lt. unfold transitive. intros n m o Hnm Hmo. induction o as [| o']. Admitted. Theorem le_Sn_le : forall n m, S n <= m -> n <= m. Proof. intros n m H. apply le_trans with (S n). - apply le_S. apply le_n. - apply H. Qed.
imports: IndProp