proposition: Lemma plus_mod_diff: forall m k x, k > 1 -> m > 0 -> x < k -> m < k -> x <> plus_mod_aux k m x.
proof: Proof. intros. destruct (le_lt_dec k (m+x)). assert (plus_mod_aux k m x = m + x - k). apply plus_mod_gt. lia. lia. lia. lia. rewrite H3. lia. assert (plus_mod_aux k m x = (m + x)%nat). apply plus_mod_lt. lia. rewrite H3. lia. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)