proposition: Theorem nat_half_plus : forall x, x > 1 -> exists a b, a > 0 /\ b <= 1 /\ x = 2 * a + b.
proof: Proof. induction x; intuition; simpl in *. lia. destruct (eq_nat_dec x 1); subst. exists 1. exists 0. intuition; lia. edestruct (IHx). lia. destruct H0. intuition. destruct x1. rewrite Nat.add_0_r in H3. exists x0. exists 1. subst. intuition; lia. exists (S x0). exists 0. subst. intuition. lia. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat