proposition: Lemma scal_correct: forall p sc a1 p1, a1 =~~= p1 -> [[scal sc a1 p]] -> fst (scal sc a1 p) =~~= EGroup.gpow p1 pG p.
proof: Proof. intros p1 sc; exact (scalb_correct p1 sc false). Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod