proposition: Lemma bits_lt_trans : forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.
proof: Proof. induction x; destruct y,z; simpl; eauto; intuition. Qed.
imports: Orders BoolOrder PeanoNat POrderedType BinNat BinInt RelationPairs EqualitiesFacts Ascii String