proposition: Lemma Code_mult_spec : Code_mult <-> forall i, i < l -> a i = b i * c i.
proof: Proof. Proof using Ha Hb Hc. unfold Code_mult; symmetry. destruct Ha as (Hlq & Ha1 & Ha2). destruct Hb as (_ & Hb1 & Hb2). destruct Hc as (_ & Hc1 & Hc2). destruct (eq_nat_dec l 0) as [ | Hl ]. + rewrite e in *; split; intros; auto; lia. + split. * intros H; right; split; try lia. exists u, u1, (r-1), r, (ca * u ⇣ ((r-1) * u1)). split; auto; split; try lia. repeat (split; auto). generalize (is_cipher_of_u Hlq); intros H2. rewrite cipher_mult_eq with (1 := Ha) (2 := H2). rewrite cipher_mult_eq with (1 := Hb) (2 := Hc). apply msum_ext; intros; rewrite H; try ring; lia. * intros [ | (_ & v & v1 & r' & r'' & p & H0 & H1 & H2 & H3 & H4) ]; try (destruct Hl; auto; fail). destruct H2 as (_ & ? & ?); subst v v1. rewrite H3 in H4. revert H4. generalize (is_cipher_of_u Hlq); intros H2. replace r' with (r-1) by lia. rewrite cipher_mult_eq with (1 := Ha) (2 := H2). rewrite cipher_mult_eq with (1 := Hb) (2 := Hc). intros E. intros i Hi. rewrite <- power_decomp_unique with (5 := E); auto; try lia. - intros; apply power_smono_l; lia. - intros j Hj; rewrite Nat.mul_1_r. apply Nat.lt_le_trans with (1 := Ha1 _ Hj), power_mono_l; lia. - intros; apply mult_lt_power_2_4; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)