proposition: Lemma lt_mod : forall a b, Zpos a < Zpos b -> (a mod b)%P = Npos a.
proof: Proof. intros a b H; rewrite Pmod_div_eucl. case (div_eucl_spec a b). assert (0 <= snd(a/b)). destruct (snd(a/b));simpl;auto with zarith. destruct (fst (a/b)). unfold Z_of_N at 1;rewrite Zmult_0_l;rewrite Zplus_0_l. destruct (snd (a/b));simpl; intros H1 H2;inversion H1;trivial. unfold Z_of_N at 1;assert (b <= p*b). pattern (Zpos b) at 1; rewrite <- (Zmult_1_l (Zpos b)). assert (H1 := Zlt_0_pos p);apply Zmult_le_compat;try lia. lia. Qed.
imports: ZArith Lia ZCmisc