proposition: Lemma nInversible_scal: forall sc a1 p1, [[scal sc a1 p1]] -> [[(a1,1%Z)]] /\ [sc].
proof: Proof. exact (nInversible_scalb false). Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod