proposition: Lemma mult_cancel_lft : forall x y z : F, z [#] [0] -> z[*]x [=] z[*]y -> x [=] y.
proof: Proof. intros x y z Hz H. apply not_ap_imp_eq. intro H2. elim (eq_imp_not_ap _ _ _ H). apply mult_lft_resp_ap; assumption. Qed.
imports: CoRN.algebra.CRings