proposition: Lemma equalBeforeTrans : forall n : rNat, transitive (rNat -> bool) (equalBefore n).
proof: Proof. intros n; red in |- *; auto with stalmarck. intros x y z H' H'0; red in |- *; auto with stalmarck. intros m H'1; apply trans_eq with (y := y m); auto with stalmarck. Qed.
imports: Coq(Relation_Definitions)