proposition: Lemma le_trans (a b c: A): le a b -> le b c -> le a c.
proof: Proof. rewrite !le_lt_eq. intros [Hlt_ab | Heq_ab] [Hlt_bc | Heq_bc]. - left; now transitivity b. - left; now subst. - left; now subst. - right; now subst. Qed.
imports: Coq(Relations RelationClasses Setoid)