proposition: Lemma plus_mod k (n:nat) (x:Finite k) : Finite k.
proof: Proof. inversion x. refine (@FinIntro k (plus_mod_aux k n x0) _). apply plus_mod_aux_fin. apply H. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)