proposition: Lemma pos_down_less_4 s : (pos_down s < 4)%positive.
proof: Proof. case s; simpl; try (intros; red; simpl; auto; fail). - intros p; case p; simpl; try (intros; red; simpl; auto; fail). - intros p; case p; simpl; try (intros; red; simpl; auto; fail). Qed.
imports: ZArith List