proposition: Fact nat_meet_powers_neq i j a b : i <> j -> a < r -> b < r -> (a*power i r)⇣(b*power j r) = 0.
proof: Proof. Proof using Hq Hr. intros Hij Ha Hb. destruct (lt_eq_lt_dec i j) as [ [] | ]; try lia. + apply nat_meet_neq_powers; auto. + rewrite nat_meet_comm. apply nat_meet_neq_powers; 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)