From df4cfc76ab059f6b3d5daf324712ad27ec281088 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 30 Apr 2013 15:53:37 +0000 Subject: [PATCH] New notation for congruence --- matita/matita/lib/arithmetics/bigops.ma | 3 ++- matita/matita/lib/arithmetics/congruence.ma | 4 ++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma index e51cd799a..1ba35c62d 100644 --- 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 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. -- 2.39.2