fact: Definition lt (t1 t2 : t) := let ft1 := fstpp(t1) in let ft2 := fstpp(t2) in let st1 := sndpp(t1) in let st2 := sndpp(t2) in if Pos.eqb ft1 ft2 then Pos.lt st1 st2 else Pos.lt ft1 ft2.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms