proposition: Theorem sum_2_power_2_injective i1 j1 i2 j2 : j1 <= i1 -> j2 <= i2 -> power i1 2 + power j1 2 = power i2 2 + power j2 2 -> i1 = i2 /\ j1 = j2.
proof: Proof. intros H1 H2 E. destruct (eq_nat_dec i1 j1) as [ H3 | H3 ]; destruct (eq_nat_dec i2 j2) as [ H4 | H4 ]. + subst j1 j2. assert (i1 = i2); auto. do 2 rewrite mult_2_eq_plus, <- power_S in E. apply power_2_inj in E; lia. + subst j1; rewrite mult_2_eq_plus in E. apply power_2_inj_1 in E; lia. + subst j2; symmetry in E. rewrite mult_2_eq_plus in E. apply power_2_inj_1 in E; lia. + revert E; apply power_inj_2; lia. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd rel_iter sums)