fact: Definition x0_neq_xH {z : Pos} : x0 z <> xH := fun p => transport (fun s => match s with xH => Empty | x0 a => z = a | x1 a => Empty end) p idpath.
imports: Basics.Overture Basics.Tactics Basics.Decidable Spaces.Nat.Core