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 h ⇒ match 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.