proposition: Lemma Le_Lt_trans : forall x y z, Le x y -> Lt y z -> Lt x z.
proof: Proof. intros x y z Hxy Hyz; case Hxy;intros. - now subst y. - eapply Lt_trans; eauto. Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)