proposition: Lemma sqrt_eq_compat_abs : forall a b, a * a = b * b -> Z.abs a = Z.abs b.
proof: Proof. intros a b E. destruct (Z.eq_dec 0 (Z.abs a + Z.abs b)) as [F|F]. lia. cut (Z.abs a - Z.abs b = 0); [ lia | ]. apply (Zmult_reg_l _ _ (Z.abs a + Z.abs b)); notzero. ring_simplify. rewrite <- Z.abs_square, <- (Z.abs_square b) in E. rewrite rewrite_power_2, E. ring. Qed.
imports: ZArith Lia Znumtheory