proposition: Fact power_2_n_ij_neq i j n : i <> j -> power (S n) 2 <> power i 2 + power j 2.
proof: Proof. intros H. destruct (lt_eq_lt_dec i j) as [ [] | ]; try tauto. + rewrite Nat.add_comm; apply power_2_inj_1; auto. + apply power_2_inj_1; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)