proposition: Theorem length_pos_lt: forall x y, (length_pos x < length_pos y)%nat -> Zpos x < Zpos y.
proof: Proof. intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac]; intros y; case y; clear y; intros y1 H || intros H; simpl length_pos; try (rewrite (Pos2Z.inj_xI x1) || rewrite (Pos2Z.inj_xO x1)); try (rewrite (Pos2Z.inj_xI y1) || rewrite (Pos2Z.inj_xO y1)); try (inversion H; fail); try (assert (Zpos x1 < Zpos y1); [apply Hrec; apply Nat.succ_lt_mono | idtac]; auto with zarith); assert (0 < Zpos y1); auto with zarith; red; auto. Qed.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic