fact: Fixpoint is_Tamari v := if v is v0 :: v' then [&& v0 <= size v', is_Tamari v' & all (fun i => nth 0 v' i + i < v0) (iota 0 v0)] else true.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype