Merge pull request #159 from mrhaandi/mod-uniform

Future proof Zlcm.v and ZMod.v for
coq-community · Apr 9, 2021 · c366d3f · c366d3f
2 parents b1add83 + 5fbc305
commit c366d3f
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/liouville/Zlcm.v b/liouville/Zlcm.v
@@ -236,7 +236,7 @@ Proof.
    reflexivity.
   assumption.
  case (Z.eq_dec a 0).
-  intro H; rewrite H; simpl; apply Zmod_0_r.
+  now intro H; rewrite H in Hap.
  intro H; clear H.
  apply Zmod0_Zdivides; assumption.
 Qed.

diff --git a/model/Zmod/ZMod.v b/model/Zmod/ZMod.v
@@ -55,7 +55,8 @@ Proof.
  case m; auto.
 Qed.
 
-Lemma Zmod_zero_rht : forall a : Z, (a mod 0)%Z = 0%Z.
+Lemma Zmod_zero_rht : forall a : Z, (a mod 0)%Z = 
+ltac:(match eval hnf in (1 mod 0) with | 0 => exact 0%Z | _ => exact a end).
 Proof.
  intro a.
  case a; auto.