(* Thanks to Constantine Plotnikov *) Require Import Arith. Require Import Euclid. Section ModuloInduction. Variable n : nat. Variable P : nat -> Prop. Hypothesis Ngt0: n > 0. Hypothesis ModBase : forall m:nat, m < n -> P (m). Hypothesis ModStep : forall m:nat, P (m) -> P(n+m). Theorem modulo_ind : forall m:nat, P(m). Proof. intro m. elim (modulo n Ngt0 m). intros r [q [MEq NNeq]]. rewrite MEq. elim q. simpl. apply ModBase. assumption. intros q1 H. simpl. rewrite plus_assoc_reverse. apply ModStep. assumption. Qed. End ModuloInduction. Print modulo_ind. Definition FQ(n:nat):Prop := (exists c3 : nat, exists c5 : nat, 8 + n = c3 * 3 + c5 * 5). Lemma FQBase : forall n:nat, n < 3 -> FQ n. Proof. intro n0. case n0. intros. exists 1. exists 1. simpl. reflexivity. intro n1. case n1. intros. exists 3. exists 0. simpl. reflexivity. intro n2. case n2. intros. exists 0. exists 2. simpl. reflexivity. intros n3 H. apply False_ind. apply (lt_n_O n3). apply lt_S_n. apply lt_S_n. apply lt_S_n. assumption. Qed. Print FQBase. Lemma FQStep : forall n, FQ n -> FQ (3 + n). Proof. intros n [c3 [c5 Eq]]. exists (S c3). exists c5. simpl. rewrite <- Eq. simpl. reflexivity. Qed. Print FQStep. Lemma FQN : forall n:nat, FQ n. Proof. intro n. apply (modulo_ind 3). auto with arith. apply FQBase. apply FQStep. Qed. Print FQN. Theorem Split3_5 : forall n : nat, 8 <= n -> exists c3, exists c5, n = c3 * 3 + c5 * 5. Proof. intros n N8. generalize (FQN (n-8)). intros [c3 [ c5 E]]. exists c3. exists c5. rewrite <- E. apply le_plus_minus . assumption. Qed. Print Split3_5.