proposition: Lemma equalBeforeLt : forall (n m : rNat) (f g : rNat -> bool), rlt n (rnext m) -> equalBefore m f g -> equalBefore n f g.
proof: Proof. intros n m f g H' H'0; red in |- *; red in H'0; auto with stalmarck. intros m0 H'1; apply H'0; auto with stalmarck. apply rltTransRnext2 with (m := n); auto with stalmarck. Qed.
imports: Coq(Relation_Definitions)