X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fcongruence.ma;h=acf873f85d0aeece079d997eab2f11a263cc1d24;hb=2c68dcfee2c3fe819c8f92a9609620a85909ce8a;hp=075a1c6c32bddbe7b79d9ee0f96a2f2fe453b038;hpb=f14ac9cceaaa7f1905f0dbc4548d24c4abe940e3;p=helm.git

diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma
index 075a1c6c3..acf873f85 100644
--- a/matita/matita/lib/arithmetics/congruence.ma
+++ b/matita/matita/lib/arithmetics/congruence.ma
@@ -15,6 +15,10 @@ definition S_mod ≝ λn,m:nat. S m \mod n.
 
 definition congruent ≝ λn,m,p:nat. mod n p = mod m p.
 
+notation "hvbox(n break ≅_{p} m)"
+  non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
 interpretation "congruent" 'congruent n m p = (congruent n m p).
 
 theorem congruent_n_n: ∀n,p:nat.congruent n n p.