Skip to content

Commit

Permalink
squeez0
Browse files Browse the repository at this point in the history
  • Loading branch information
bmtrager committed Oct 28, 2023
1 parent f920fe2 commit efe522a
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion coq/FHE/encode.v
Original file line number Diff line number Diff line change
Expand Up @@ -2322,7 +2322,15 @@ Section norms.
(x <= R0)%O ->
x = 0.
Proof.
Admitted.
intros.
apply Rle_antisym.
- rewrite /Order.le/= in H0.
move /RlebP in H0.
by replace (R0) with (IZR (Z0)) in H0 by lra.
- rewrite /Order.le/= in H.
move /RlebP in H.
by replace (R0) with (IZR (Z0)) in H by lra.
Qed.

Lemma canon_norm_zer_mod_qpoly n (p : {poly R}) :
canon_norm_inf n p = 0 ->
Expand Down

0 comments on commit efe522a

Please sign in to comment.