proposition: Lemma Rdiv_compat_r : forall a b c : R, a <> 0 -> c <> 0 -> (a*b) / (a*c) = b/c.
proof: Proof. intros a b c Ha Hc. field. apply conj. apply Hc. apply Ha. Qed.
imports: Coq(Reals) Flocq(Core) Gappa(Gappa_tactic) Interval(Tactic)