proposition: Lemma div_eucl_spec : forall a b, Zpos a = fst (a/b)%P * b + snd (a/b)%P /\ snd (a/b)%P < b.
proof: Proof. Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || lia). intros a b;generalize a;clear a;induction a;simpl;zsimpl. case IHa; destruct (a/b)%P as [q r]. case q; case r; simpl fst; simpl snd. rewrite Zmult_0_l; rewrite Zplus_0_r; intros HH; discriminate HH. intros p H; rewrite H; match goal with | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto. rewrite PminusN_le... generalize H1; zsimpl; auto. rewrite PminusN_le... intros p H; rewrite H; match goal with | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring. ring_simplify. case (Zle_lt_or_eq _ _ H1); auto with zarith. intros p p1 H; rewrite H. match goal with | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring. rewrite PminusN_le... generalize H1; zsimpl; auto. rewrite PminusN_le... case IHa; destruct (a/b)%P as [q r]. case q; case r; simpl fst; simpl snd. rewrite Zmult_0_l; rewrite Zplus_0_r; intros HH; discriminate HH. intros p H; rewrite H; match goal with | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto. rewrite PminusN_le... generalize H1; zsimpl; auto. rewrite PminusN_le... intros p H; rewrite H; simpl; intros H1; split; auto. zsimpl; ring. intros p p1 H; rewrite H. match goal with | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl; intros H1 H2; split; zsimpl; auto; try ring. rewrite PminusN_le... generalize H1; zsimpl; auto. rewrite PminusN_le... match goal with | [|- context [ ?xx ?< b ]] => generalize (is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end; zsimpl; simpl. split; auto. case (Zle_lt_or_eq 1 b). 2-3: auto with zarith. generalize (Zlt_0_pos b); auto with zarith. Qed.
imports: ZArith Lia ZCmisc