proposition: Theorem Ksqr_eq: forall x y, x^2 = y^2 -> x = y \/ x = - y.
proof: Proof. intros x y H. case (@Kmult_integral (x - y) (x + y)); auto. ring [H]. intros H1; left; apply trans_equal with (y + (x - y)); try ring. rewrite H1; ring. intros H1; right; apply trans_equal with (-y + (x + y)); try ring. rewrite H1; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith