proposition: Fact is_cipher_of_inj f1 f2 a : is_cipher_of f1 a -> is_cipher_of f2 a -> forall i, i < l -> f1 i = f2 i.
proof: Proof. intros (H1 & H2 & H3) (_ & H4 & H5). rewrite H3 in H5. revert H5; apply power_decomp_unique. + apply (@power_mono_l 1 _ 2); lia. + intros; apply power_smono_l; lia. + intros i Hi; apply Nat.lt_le_trans with (1 := H2 _ Hi), power_mono_l; lia. + intros i Hi; apply Nat.lt_le_trans with (1 := H4 _ Hi), 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)