proposition: Lemma is_lcm_moduplus k p q g l u : 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 H2 H3 H4. induction k as [ | k IHk ]. + simpl; do 2 rewrite Nat.add_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) by (simpl; lia). apply is_lcm_plus with (g := g); auto. apply is_gcd_moduplus; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)