Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
bmtrager committed Jan 16, 2024
1 parent 9b1f2e1 commit b269e62
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions coq/FHE/zp_prim_root.v
Original file line number Diff line number Diff line change
Expand Up @@ -2917,9 +2917,9 @@ Section add_self_pow.
unfold is_partitioned_in_same_bins_by_m_to.
intros.
rewrite !mxE /rotate_index_right_ord.
assert (val i == val j %[mod 2^m.+1] \/ val i + 2^m == val j %[mod 2^m.+1]).
assert (val i == val j %[mod 2^m.+1] \/ val i == val j + 2^m %[mod 2^m.+1]).
{
admit.
by apply vals_mod_2_Sn.
}
destruct H1.
- rewrite (H _ _ H1).
Expand Down

0 comments on commit b269e62

Please sign in to comment.