proposition: Lemma ainv0 : ainv 0 == 0.
proof: Proof. apply: sup_default => -[_ [z ub_z]]. by have [a /notK[]] := cut_ub z; apply/leRq/ub_z; rewrite amul0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)