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