proposition: Lemma div4_exact : forall n:nat, let (q, r) := div4 n in n = 4 * q + r.
proof: Proof. intros n; elim n using div4_ind; try (simpl in |- *; auto; fail). intros p; cbv beta iota zeta delta [div4] in |- *; fold div4 in |- *. case (div4 p). intros q r Hrec; rewrite Hrec; ring. Qed.
imports: Arith ArithRing Lia