proposition: Lemma eq_div : forall (x y u v : F) y_ v_, x[*]v [=] u[*]y -> (x[/] y[//]y_) [=] (u[/] v[//]v_).
proof: Proof. intros x y u v Hy Hv H. astepl (x[*][1][/] y[//]Hy). astepl (x[*] (v[/] v[//]Hv) [/] y[//]Hy). astepl ((x[*]v[/] v[//]Hv) [/] y[//]Hy). astepl ((u[*]y[/] v[//]Hv) [/] y[//]Hy). astepl ((u[*]y[/] y[//]Hy) [/] v[//]Hv). astepl (u[*] (y[/] y[//]Hy) [/] v[//]Hv). Step_final (u[*][1][/] v[//]Hv). Qed.
imports: CoRN.algebra.CRings