proposition: Lemma RpmsS_prod x y : inc x BRps -> inc y BRms -> inc (x *r y) BRms.
proof: Proof. move => sa sb. move:(BRopp_negative1 sb) => sd. rewrite /BRprod (Y_false (BRps_nz sa)) (Y_true sa). rewrite (Y_false (BRms_nz sb)) (Y_false (BR_di_neg_spos sb)). rewrite - (BR_prod_aux1 sa sd); move:(RpsS_prod sa sd); apply:BRopp_positive1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)