proposition: Lemma Stern_consecutive_coprime2 a b : 0 < a -> 0 < b -> coprime a b -> Stern_consecutive a b.
proof: Proof. wlog: a b / a < b. move => h; case: (ltngtP a b) => ha hb hc hd. + by apply: h. + by apply:Stern_consecutive_sym; apply: h => //; rewrite coprime_sym. + by move: hd; rewrite /coprime - ha gcdnn => /eqP ->; exists 0,0. elim: b a {-2} b (leqnn b). move => a b; rewrite leqn0 => /eqP -> //. move=> n H b a lan lab bp ap. rewrite - coprime_modr coprime_sym => cp. have ha: (a %% b < b) by rewrite ltn_mod bp. move: (leq_trans lab lan); rewrite ltnS => hb. case :(posnP (a %% b)) =>hc. move: cp;rewrite hc/coprime gcd0n => /eqP ->. rewrite -(prednK ap); apply: Stern_consecutive_1n. rewrite (divn_eq a b); apply:Stern_consecutive_rec; apply:Stern_consecutive_sym. exact: (H (a %% b) b hb ha hc bp cp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)