proposition: Lemma lt_le_trans {A:Type}{le:relation A}{P:PreOrder le}: forall a b c, lt a b -> le b c -> lt a c.
proof: Proof. intros a b c [Hab H'ab] Hbc; split. - now transitivity b. - intro H; destruct H'ab; now transitivity c. Qed.