fact: Definition complete v0 h vn := [/\ valid h, gapless h, continuous v0 h & last_atval v0 h = vn].
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)