proposition: Lemma is_lcm_modulus k p q g l u : k*p <= q -> p = u*g -> is_gcd p q g -> is_lcm p q l -> is_lcm p (q-k*p) (l-k*u*p).
proof: Proof. rewrite <- Nat.mul_assoc. intros H1 H2 H3 H4. revert H1. induction k as [ | k IHk ]; intros H1. + simpl; do 2 rewrite Nat.sub_0_r; auto. + replace (q - S k*p) with (q -k*p -p) by (simpl; lia). replace (l - S k*(u*p)) with (l - k*(u*p) - u*p). - apply is_lcm_minus with (g := g); auto. * simpl in H1; lia. * apply is_gcd_modulus; auto. simpl in H1; lia. * apply IHk; simpl in H1; lia. - simpl; generalize (u*p) (k*(u*p)); intros; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)