proposition: Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
proof: Proof. unfold lt, eq; intros x y z Hxy Hyz. destruct (compare x z) eqn:Hxz; auto. - rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz. rewrite (compare_trans Hxz Hyz) in Hxy; discriminate. - rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy. rewrite (compare_trans Hxy Hxz) in Hyz; discriminate. Qed.
imports: OrderedType Orders