proposition: Lemma nat_4_dec : forall n, exists k, (4 * k = n \/ 4 * k + 1= n \/ 4 * k + 2 = n \/ 4 * k + 3 = n )%nat.
proof: Proof. induction n. exists 0%nat. left. intuition. destruct IHn as [k [H | [H| [H|H]]]]. exists k. right. left. intuition lia. exists k. right. right. left. intuition lia. exists k. right. right. right. intuition lia. exists (S k). left. intuition lia. Qed.
imports: Ctacfield Cbase Cpow Lia