proposition: Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p.
proof: Proof. apply/val_inj => /=. by rewrite subr0 mulr1 opprB addrCA subrr addr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed