proposition: Lemma comparabler_trans : transitive (comparable : rel R).
proof: Proof. move=> y x z; rewrite !comparablerE => xBy_real yBz_real. by have := rpredD xBy_real yBz_real; rewrite addrA addrNK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)