proposition: Lemma BRprod_1l x: realp x -> \1r *r x = x.
proof: Proof. have H: forall x, inc x BRps -> \1r *r x = x. move => y yp; move: (BRps_sBR yp) => yq. rewrite (BR_prodQ_aux QpsS1 yp); set_extens t. by move => /funI_P [z zy ->]; rewrite (BQprod_1l (BRi_sQ yq zy)). by move => ty; apply/funI_P; ex_tac; rewrite (BQprod_1l (BRi_sQ yq ty)). case/BR_i1P; [ by move => ->;rewrite BRprod_0r | by apply: H | ]. move => h; move: (BRopp_negative1 h) => /H. move: (BRms_sBR h) => xq; move:(RSp RS1 xq) => hq. by rewrite - (BRopp_prod_r RS1 xq);apply:BRopp_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)