proposition: Lemma p_of_rs1P r s : reflect (r = 1%:pr /\ s = 1%:pr) ([p_of r, s] == 1%:pr).
proof: Proof. move: (p_of_rs1 r s) ->. apply: (iffP idP); [by case/andP => /eqP -> /eqP -> | by case => -> ->; rewrite eqxx]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)