proposition: Lemma plength_spec l : Pos.to_nat (@plength elt l) = S (length l).
proof: Proof. unfold plength. rewrite plength_aux_spec. apply Nat.add_1_r. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)