proposition: Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
proof: Proof. intros n m p. rewrite 3 lt_eq_cases. intros [LT|EQ] [LT'|EQ']; try rewrite EQ; try rewrite <- EQ'; generalize (lt_trans n m p); auto with relations. Qed.
imports: NZAxioms NZBase Decidable OrdersTac