use [positive] for [F] modulus, char_ge_C instead of char_gt_C

3 files changed, 22 insertions, 11 deletions

diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v
index f3a43f3e3..13a0ffa95 100644
--- a/src/Algebra/Field_test.v
+++ b/src/Algebra/Field_test.v
@@ -42,7 +42,7 @@ Module _fsatz_test.
     Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0. fsatz. Qed.
     Import BinNums.
 
-    Context {char_gt_15:@Ring.char_gt F eq zero one opp add sub mul 15}.
+    Context {char_ge_16:@Ring.char_ge F eq zero one opp add sub mul 16}.
 
     Local Notation two := (one+one) (only parsing).
     Local Notation three := (one+one+one) (only parsing).
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index 8110ad5cd..72414b46e 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -62,21 +62,21 @@ Module IntegralDomain.
       Qed.
 
       Section WithChar.
-        Context C (char_gt_C:@Ring.char_gt R eq zero one opp add sub mul C).
+        Context C (char_ge_C:@Ring.char_ge R eq zero one opp add sub mul C) (HC: Pos.lt xH C).
         
         Definition is_factor_nonzero (n:N) : bool :=
-          match n with N0 => false | N.pos p => BinPos.Pos.leb p C end.
+          match n with N0 => false | N.pos p => BinPos.Pos.ltb p C end.
         Lemma is_factor_nonzero_correct (n:N) (refl:Logic.eq (is_factor_nonzero n) true)
           : of_Z (Z.of_N n) <> zero.
         Proof.
-          destruct n; [discriminate|]; rewrite Znat.positive_N_Z; apply char_gt_C, Pos.leb_le, refl.
+          destruct n; [discriminate|]; rewrite Znat.positive_N_Z; apply char_ge_C, Pos.ltb_lt, refl.
         Qed.
 
         Lemma RZN_product_nonzero l (H : forall x : N, List.In x l -> of_Z (Z.of_N x) <> zero)
           : of_Z (Z.of_N (List.fold_right N.mul 1%N l)) <> zero.
         Proof.
           rewrite <-List.Forall_forall in H; induction H; simpl List.fold_right.
-          { eapply char_gt_C, Pos.le_1_l. }
+          { eapply char_ge_C; assumption. }
           { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism constr:(of_Z).
             eapply Ring.nonzero_product_iff_nonzero_factor; eauto. }
         Qed.
@@ -106,7 +106,7 @@ Module IntegralDomain.
           | Coef_mul c1 c2 => andb (is_nonzero c1) (is_nonzero c2)
           | _ => is_constant_nonzero (CtoZ c)
           end.
-        Lemma is_nonzero_correct c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero.
+        Lemma is_nonzero_correct' c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero.
         Proof.
           induction c;
             repeat match goal with
@@ -123,6 +123,17 @@ Module IntegralDomain.
                    end.
         Qed.
       End WithChar.
+
+      Lemma is_nonzero_correct
+            C
+            (char_ge_C:@Ring.char_ge R eq zero one opp add sub mul C)
+            c (refl:Logic.eq (andb (Pos.ltb xH C) (is_nonzero C c)) true)
+        : denote c <> zero.
+      Proof.
+        rewrite Bool.andb_true_iff in refl; destruct refl.
+        eapply @is_nonzero_correct'; try apply Pos.ltb_lt; eauto.
+      Qed.
+
     End ReflectiveNsatzSideConditionProver.
 
     Ltac reify one opp add mul x :=
@@ -145,9 +156,9 @@ Module IntegralDomain.
   Ltac solve_constant_nonzero :=
     match goal with
     | |- not (?eq ?x _) =>
-      let cg := constr:(_:Ring.char_gt (eq:=eq) _) in
+      let cg := constr:(_:Ring.char_ge (eq:=eq) _) in
       match type of cg with
-        @Ring.char_gt ?R eq ?zero ?one ?opp ?add ?sub ?mul ?C =>
+        @Ring.char_ge ?R eq ?zero ?one ?opp ?add ?sub ?mul ?C =>
         let x' := _LargeCharacteristicReflective.reify one opp add mul x in
         let x' := constr:(@_LargeCharacteristicReflective.denote R one opp add mul x') in
         change (not (eq x' zero));
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
index f39d730f2..640b12ed9 100644
--- a/src/Algebra/Ring.v
+++ b/src/Algebra/Ring.v
@@ -388,11 +388,11 @@ Section of_Z.
   Qed.
 End of_Z.
 
-Definition char_gt
+Definition char_ge
            {R eq zero one opp add} {sub:R->R->R} {mul:R->R->R}
            C :=
-  @Algebra.char_gt R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C.
-Existing Class char_gt.
+  @Algebra.char_ge R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C.
+Existing Class char_ge.
 
 (*** Tactics for ring equations *)
 Require Export Coq.setoid_ring.Ring_tac.