proposition: Lemma opp_ind E : (forall x, E (- x) -> E x) -> (forall x, x >= 0 -> E x) -> forall x, E x.
proof: Proof. by move=> IHopp IHpos x; case: (ltcP x 0) gec0_opp; auto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)