proposition: Fact base_p_uniq l1 l2 : Forall2 (fun x y => x < p /\ y < p) l1 l2 -> expand p l1 = expand p l2 -> l1 = l2.
proof: Proof. Proof using Hp. induction 1 as [ | x1 x2 l1 l2 H1 H2 IH2 ]; auto; simpl; intros H3. rewrite (Nat.add_comm x1), (Nat.add_comm x2), (Nat.mul_comm p), (Nat.mul_comm p) in H3. apply div_rem_uniq in H3; try lia. destruct H3 as [ H3 ]; subst; f_equal; auto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)