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