proposition: Fact nat_meet_powers_eq i a b : (a*power i r)⇣(b*power i r) = (a⇣b)*power i r.
proof: Proof. Proof using Hr. rewrite Hr, <- power_mult, nat_meet_mult_power2; 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)