New notation for congruence

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index e51cd799aa11533605db577807b5165ffdd6aff5..1ba35c62d31cbe04d1eb1aaae64b044ba64e87e9 100644 (file)
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -241,7 +241,8 @@ theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat →
      >Hp1 >(mod_plus_times …) /2 by refl, monotonic_lt_minus_l, eq_f/
   |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2 by plus_minus/
-   #eqi >eqi in ⊢ (???%); >div_plus_times /2 by refl, monotonic_lt_minus_l, trans_eq/ 
+   #eqi >eqi in ⊢ (???%); >div_plus_times 
+   /2 by refl, monotonic_lt_minus_l, trans_eq/ 
   ]
 qed.
 

diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma
index 075a1c6c32bddbe7b79d9ee0f96a2f2fe453b038..acf873f85d0aeece079d997eab2f11a263cc1d24 100644 (file)
--- 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.