Require Import Arith. (* with 3-dollar and 5-dollar notes, we have exact change for any amount greater or equal to 8 dollars *) Theorem coins: forall m:nat, exists i:nat, exists j:nat, ((plus 8 m) =(plus (mult i 5) (mult j 3))). (* By induction on m *) intro m; elim m. (* 8 = 1*5 + 1*3 *) exists 1; exists 1. simpl; auto. (* Induction hypothesis *) intros n H'; elim H'. (* extracting witnesses from H' *) intros i E ; elim E; intros j Ind; clear E H'. (* On réécrit avec cette hypothese dans le but *) rewrite <- plus_n_Sm. rewrite Ind. (* At least 1 5-dollar note ? *) generalize Ind. case i. clear Ind. intro Ind; simpl. (* intro i1; intro Ind.*) (* At least 1 3-dollar note ? (j=(S j1) *) generalize Ind; case j; clear Ind; [idtac | intro j1]; intro Ind. (* (0,0) impossible *) inversion Ind. (* At least 2 notes of 3 (j = (S (S j2)) ? *) generalize Ind; case j1; clear Ind; [idtac | intro j2]; intro Ind. (* (0,1) impossible *) inversion Ind. (* At least 3 notes of 3 (j = (S (S (S j3)))) *) generalize Ind; case j2; clear Ind; [idtac | intro j3]; intro Ind. (* (0,2) impossible *) inversion Ind. (* We have at least 3 "3-dollar notes", we replace these 3 by 2 "5-dollar notes *) (* easy for #(5-dollar notes)=0 *) exists 2 ; exists j3. simpl; auto. intros i0 H0. (* We have at least 1 "5-dollar" note, we replace it by 2 "3-dollar" note *) exists i0; exists (plus 2 j). simpl; repeat rewrite <- plus_n_Sm; auto. Qed.