Add

ajreynol · Feb 24, 2025 · a577f28 · a577f28
1 parent 62a7349
commit a577f28
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/proofs/eo/cpc/rules/Rewrites.eo b/proofs/eo/cpc/rules/Rewrites.eo
@@ -175,6 +175,11 @@
   :args (t1 c1 cc1)
   :conclusion (= (>= (to_real t1) c1) (>= t1 cc1))
 )
+(declare-rule arith-divisible-elim ((n1 Int) (t1 Int))
+  :premises ((= (= n1 0) false))
+  :args (n1 t1)
+  :conclusion (= (divisible n1 t1) (= (mod_total t1 n1) 0))
+)
 (declare-rule arith-abs-eq ((@T0 Type) (@T1 Type) (x1 @T0) (y1 @T1))
   :args (x1 y1)
   :conclusion (= (= (abs x1) (abs y1)) (or (= x1 y1) (= x1 (- y1))))