proposition: Lemma pell_theory: ell_theory pkO pkI pkplus pkmul pksub pkopp pkinv pkdiv pA pB pis_zero.
proof: Proof. constructor. apply pKfth. apply pNonSingular. exact pone_not_zero. exact ptwo_not_zero. exact pis_zero_correct. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod