proposition: Lemma gec0N_eq0 x : x >= 0 -> - x >= 0 -> x == 0.
proof: Proof. by move/leRq=> le0x /leRq/leR_opp2; rewrite oppK opp0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)