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