proposition: Lemma plus_mod_aux_fin k n (x:nat): (x < k) -> plus_mod_aux k n x < k.
proof: Proof. generalize dependent k. generalize dependent x. induction n. auto. intros. simpl. destruct k. lia. simpl. destruct (Nat.eq_dec (S k) (S x)). auto. inversion e. rewrite Nat.sub_diag. apply IHn. auto. lia. assert (k - x <> O) by lia. set (k - x) as diff. fold diff in H0. destruct diff. firstorder. apply IHn. lia. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.Default(AlmostFull) AlmostFull.Default(AFConstructions)