proposition: Lemma plus_mod_suc m: forall x, x < m -> plus_mod_aux (S m) m (S x) = x.
proof: Proof. intros. assert (S m = (1 + m)%nat). firstorder. rewrite H0. assert (S x = (1 + x)%nat). firstorder. rewrite H1. apply plus_mod_wraparound. firstorder. firstorder. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)