proposition: Lemma binary : strategy.
proof: Proof. refine (mkstrat (fun n h => match quotient two _ n with | exist n0 e => 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.
imports: strategies Arith euclid shift Euclid Le_lt_compl Mult_compl Constants