(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/congruence".
+set "baseuri" "cic:/matita/library_auto/nat/congruence".
include "nat/relevant_equations.ma".
include "nat/primes.ma".
\lambda n,m,p:nat. mod n p = mod m p.
interpretation "congruent" 'congruent n m p =
- (cic:/matita/nat/congruence/congruent.con n m p).
+ (cic:/matita/library_auto/nat/congruence/congruent.con n m p).
notation < "hvbox(n break \cong\sub p m)"
(*non associative*) with precedence 45