proposition: Lemma BR_prod_aux1 x y : inc x BRps -> inc y BRps -> (x *r y) = (BRprod_aux x y).
proof: Proof. move => pa pb. move /BRps_iP:(pa) => [_ xnz]. move /BRps_iP:(pb) => [_ ynz]. by rewrite /BRprod; repeat Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)