proposition: Fact power_2_inj i j : power i 2 = power j 2 -> i = j.
proof: Proof. intros H. destruct (lt_eq_lt_dec i j) as [ [ C | C ] | C ]; auto; apply power_smono_l with (x := 2) in C; lia. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd rel_iter sums)