proposition: Lemma mult_cancel_rht : forall x y z : F, z [#] [0] -> x[*]z [=] y[*]z -> x [=] y.
proof: Proof. intros x y z Hz H. apply (mult_cancel_lft x y z). assumption. astepr (y[*]z). Step_final (x[*]z). Qed.
imports: CoRN.algebra.CRings