proposition: Theorem rdiv6 a b : ~ a == 0 -> ~ b == 0 -> / (a / b) == b / a.
proof: Proof. intros H H0. assert (Hk : ~ a / b == 0). { contradict H. transitivity (b * (a / b)). - now rewrite rdiv_simpl. - rewrite H. apply rmul_0_r. } apply rmul_reg_l with (a / b); trivial. rewrite (rmul_comm (a / b)), rinv_l; trivial. rewrite !rdiv_def. transitivity (/ a * a * (/ b * b)); [ | ring ]. now rewrite !rinv_l, rmul_1_l. Qed.
imports: ZArith_base