proposition: Lemma oppK x : - (- x) == x.
proof: Proof. split=> [a /open[b ltxb ltba] | a [b lt_na_b le_b_nx]]. by exists (- b)%R => [|[c]]; rewrite ?ltr_opp2 ?opprK => // /(ltc_trans ltxb). by apply/notK=> leax; case: le_b_nx; exists a; rewrite // ltr_oppl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)