proposition: Lemma Code_plus_spec : Code_plus <-> forall i, i < l -> a i = b i + c i.
proof: Proof. Proof using Ha Hb Hc. symmetry; unfold Code_plus. destruct Ha as (H & Ha1 & Ha2). destruct Hb as (_ & Hb1 & Hb2). destruct Hc as (_ & Hc1 & Hc2). destruct (eq_nat_dec l 0) as [ | Hl ]. + clear Hc Hb Ha. subst l; rewrite msum_0 in *; split; intros; lia. + rewrite Hc2, Ha2, Hb2, <- sum_0n_distr_in_out. split. * intros; apply msum_ext; intros; f_equal; auto. * intros E i Hi. apply power_decomp_unique with (i := i) in E; auto; try lia; clear i Hi. - intros; apply power_smono_l; lia. - intros i Hi; apply Nat.lt_le_trans with (1 := Ha1 _ Hi), power_mono_l; lia. - intros i Hi. apply Nat.lt_le_trans with (power (S q) 2). ++ rewrite power_S, <- mult_2_eq_plus. generalize (Hb1 _ Hi) (Hc1 _ Hi); lia. ++ apply power_mono_l; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)