proposition: Lemma plength_aux_spec l p : Pos.to_nat (@plength_aux elt l p) = length l + Pos.to_nat p.
proof: Proof. revert p. induction l; trivial. simpl plength_aux. intros. now rewrite IHl, Pos2Nat.inj_succ, Nat.add_succ_r. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)