proposition: Lemma square_id : forall (F : CField) (x : F), x[^]2 [=] x -> {x [=] [0]} + {x [=] [1]}.
proof: Proof. intros F x H. cut (([0]:F) [#] ([1]:F)). intro H0. elim (ap_cotransitive_unfolded _ _ _ H0 x). intro H1. right. apply not_ap_imp_eq. red in |- *. intro H2. set (H3 := minus_resp_ap_rht F x [1] [1] H2) in *. set (H4 := ap_wdr_unfolded F (x[-][1]) ([1][-][1]) [0] H3 (cg_minus_correct F [1])) in *. set (H5 := ap_symmetric_unfolded F [0] x H1) in *. set (H6 := mult_resp_ap_zero F x (x[-][1]) H5 H4) in *. simpl in |- *. set (H7 := x_xminone F x H) in *. set (H8 := eq_imp_not_ap F (x[*] (x[-][1])) [0] H7) in *. intuition. left. apply not_ap_imp_eq. red in |- *. intro H2. set (H3 := minus_resp_ap_rht F x [1] [1] b) in *. set (H4 := ap_wdr_unfolded F (x[-][1]) ([1][-][1]) [0] H3 (cg_minus_correct F [1])) in *. set (H6 := mult_resp_ap_zero F x (x[-][1]) H2 H4) in *. set (H7 := x_xminone F x H) in *. set (H8 := eq_imp_not_ap F (x[*] (x[-][1])) [0] H7) in *. intuition. apply ap_symmetric_unfolded. apply ring_non_triv. Qed.
imports: CoRN.algebra.CRings