proposition: Lemma is_lcm_plus p q g l u : p = u*g -> is_gcd p q g -> is_lcm p q l -> is_lcm p (q+p) (l+u*p).
proof: Proof. destruct (eq_nat_dec g 0) as [ H0 | H0 ]. + intros _ H1 H2. subst; apply is_gcd_0 in H1. destruct H1; subst; simpl. rewrite Nat.mul_0_r, Nat.add_0_r; auto. + intros H2 H3 H4. apply is_gcd_mult_lcm with (1 := H0). * apply is_gcd_plus; auto. * do 2 rewrite Nat.mul_add_distr_l. rewrite <- (is_gcd_lcm_mult H3 H4). f_equal. rewrite H2 at 2. rewrite Nat.mul_assoc, (Nat.mul_comm g); auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)