proposition: Theorem div4_ind : forall P:nat -> Prop, P 0 -> P 1 -> P 2 -> P 3 -> (forall n:nat, P n -> P (S (S (S (S n))))) -> forall n:nat, P n.
proof: Proof. intros P P0 P1 P2 P3 Prec n. cut (P n /\ P (S n) /\ P (S (S n)) /\ P (S (S (S n)))). - intuition. - elim n; intuition. Qed.
imports: Arith ArithRing Lia