proposition: Theorem KLroot_root: forall r, match KLroot r with None => forall k, kmul k k <> r | Some k => kmul k k = r end.
proof: Proof. intros r; generalize (Kfind_root_root r LK); unfold KLroot; case Kfind_root; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith