definition congruent: nat \to nat \to nat \to Prop \def
\lambda n,m,p:nat. mod n p = mod m p.
-interpretation "congruent" 'congruent n m p =
- (cic:/matita/library_autobatch/nat/congruence/congruent.con n m p).
+interpretation "congruent" 'congruent n m p = (congruent n m p).
notation < "hvbox(n break \cong\sub p m)"
(*non associative*) with precedence 45