Use floor from Coqlib

Author: xavierleroy

cfrontend/Ctypes.v

@@ -460,8 +460,6 @@ Definition bitalignof_intsize (sz: intsize) : Z :=
   | I32 => 32
   end.
 
-Definition floor (n: Z) (amount: Z) := (n / amount) * amount.
-
 Definition next_field (pos: Z) (m: member) : Z :=
   match m with
   | Member_plain _ t =>
@@ -495,20 +493,6 @@ Definition layout_field (pos: Z) (m: member) : res (Z * bitfield) :=
 
 (** Some properties *)
 
-Lemma floor_interval:
-  forall x y, y > 0 -> floor x y <= x < floor x y + y.
-Proof.
-  unfold floor; intros.
-  generalize (Z_div_mod_eq x y H) (Z_mod_lt x y H).
-  set (q := x / y). set (r := x mod y). intros. lia.
-Qed.
-
-Lemma floor_divides:
-  forall x y, y > 0 -> (y | floor x y).
-Proof.
-  unfold floor; intros. exists (x / y); auto.
-Qed.
-
 Lemma bitalignof_intsize_pos:
   forall sz, bitalignof_intsize sz > 0.
 Proof.