proposition: Lemma Lt_not_Gt : forall x y, Lt x y -> ~ Lt y x.
proof: Proof. intros x y H H'; case (Lt_irreflexive (a:=x)). eapply Lt_trans; eauto. Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)