proposition: Lemma Lt_Le_trans : forall x y z, Lt x y -> Le y z -> Lt x z.
proof: Proof. intros x y z Hxy Hyz; destruct Hyz as [H0 | H]. - now subst. - eapply Lt_trans; eauto. Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)