proposition: Lemma Pmod_div_eucl : forall a b, a mod b = snd (a/b).
proof: Proof. Proof with auto. intros a b;generalize a;clear a;induction a;simpl; try (rewrite IHa; assert (H1 := div_eucl_spec a b); destruct (a/b) as [q r]; destruct q as [|q];destruct r as [|r];simpl in *; match goal with | [|- context [ ?xx ?< b ]] => assert (H2 := is_lt_spec xx b);destruct (xx ?< b) | _ => idtac end;simpl) ... destruct H1 as [H3 H4];discriminate H3. destruct (1 ?< b);simpl ... Qed.
imports: ZArith Lia ZCmisc