proposition: Fact g_nlb_fun n l1 l2 : g_nlb n l1 -> g_nlb n l2 -> l1 = l2.
proof: Proof. intros H1 H2; revert H1 l2 H2. induction 1; inversion 1; auto; try lia; f_equal; auto. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)