proposition: Lemma eqr_div (R : numFieldType) (x y z t : R): y != 0 -> t != 0 -> (x / y == z / t) = (x * t == z * y).
proof: Proof. move=> yD0 tD0. rewrite -[x in RHS](divfK yD0) -[z in RHS](divfK tD0) mulrAC. by apply/eqP/eqP=> [->//|xyty]; exact/(mulIf tD0)/(mulIf yD0). Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp