proposition: Fact nat_meet_power2_neq x y : x <> y -> (power x 2) ⇣ (power y 2) = 0.
proof: Proof. intros H. destruct (lt_eq_lt_dec x y) as [[]|]; try lia. + apply nat_meet_power2_lt; auto. + rewrite nat_meet_comm; apply nat_meet_power2_lt; 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)