proposition: Lemma mod_le_a : forall a b r, a mod b = r -> r <= a.
proof: Proof. intros a b r H;generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl; rewrite H;simpl;intros (H1,H2). assert (0 <= fst (a / b) * b). destruct (fst (a / b));simpl;auto with zarith. auto with zarith. Qed.
imports: ZArith Lia ZCmisc