proposition: Lemma plus_mod_wraparound (m:nat): forall x n, x < m -> n > 0 -> plus_mod_aux (n + m) m (n + x) = x.
proof: Proof. induction m. intros; lia. intros. simpl. remember (n + S m - (S (n + x))) as diff. destruct diff. assert (m = x). lia. rewrite H1. assert (plus_mod_aux (n + S x) x O = (x + O)%nat). apply plus_mod_lt. lia. lia. assert (plus_mod_aux (S n + m) m (S n + x) = x). apply IHm. lia. lia. assert ((S n + m)%nat = (n + S m)%nat). lia. rewrite <- H2. assert (S (n+x) = (S n + x)%nat). lia. rewrite H3. apply H1. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)