proposition: Theorem Kfind_root_root: forall r l, match Kfind_root r l with None => forall k, In k l -> kmul k k <> r | Some k => kmul k k = r end.
proof: Proof. intros r l; elim l; simpl. intros k H; case H. intros a l1 Hrec; generalize (Eth.(is_zero_correct) (ksub r (kmul a a))); case is_zero; intros HH; case HH; clear HH; intros H1 H2. apply trans_equal with (ksub r kO); [rewrite <- H1; auto | idtac]; ring. generalize Hrec; case Kfind_root; auto. intros H3 k [H4 | H4]; subst; auto. intros H4; absurd (false = true); try (intro HH; discriminate). apply H2; subst; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith