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. - induction y; destruct z; simpl; eauto; intuition. - induction y; destruct z; simpl; eauto; intuition. - induction y; destruct z; simpl; eauto; intuition. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec