proposition: Lemma R_mult_strext : bin_op_strext _ R_mult.
proof: Proof. red in |- *; red in |- *. intros x y a b Hap. elim (ap_cotransitive_unfolded _ _ _ Hap (R_mult x b)); intro H. right; apply R_mult_rht_ext with x; auto. left; apply R_mult_lft_ext with b; auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection