# Library Additions.binary_strat

Require Import strategies.
Require Import Arith.
Require Import euclid.
Require Import shift.
Require Import Euclid.
Require Import Le_lt_compl.
Require Import Mult_compl.
Require Import Constants.

Lemma binary : strategy.
Proof.
refine
(mkstrat
(fun n hmatch quotient two _ n with
| exist n0 _exist _ n0 _
end)).
auto with arith.
elim e; simple induction 1; intros H1 H2.
case (enum1 x H2); intro H3.

cut (n = n0 × two); [ intro eg | idtac ].
cut (two n0); [ intro H'1 | idtac ].
split; auto.
rewrite eg; apply mult_p_lt_pq.
apply lt_le_trans with 2; auto with arith.
auto with arith.
apply not_lt_le; unfold not in |- *; intro.
absurd (n < four); [ apply lt_asym; auto with arith | idtac ].
rewrite eg; replace four with (two × two).
apply mult_lt_r.
auto with arith.
auto with arith.
simpl in |- *; auto with arith.
rewrite (plus_n_O (n0 × two)); elim H3; auto with arith.

cut (two n0); [ intro H'1 | idtac ].
split; [ idtac | auto with arith ].
rewrite H1; rewrite mult_comm; apply lt_b_qbr.
rewrite H3; auto with arith.
auto with arith.
apply lt_le_trans with two; [ idtac | auto with arith ].
rewrite H3; auto with arith.
apply not_lt_le; unfold not in |- *; intro.
cut (n three).
intro; absurd (four < three);
[ unfold four, three in |- *; auto with arith | idtac ].
apply lt_le_trans with n; auto with arith.
replace three with (one × two + x).
rewrite H1; auto with arith.
rewrite H3; simpl in |- *; auto with arith.
Qed.