proposition: Lemma CF_unique a a' l l' : good_for_cf a l -> good_for_cf a' l' -> SCF (a::l) = SCF(a'::l') -> a::l = a'::l'.
proof: Proof. wlog : a a' l l'/ (size l <= size l')%N. move => H; case/orP:(leq_total (size l) (size l')); first by apply: H. by move => ha hb hc /esym hd; symmetry; apply:H. move => ss ha hb sv. move/andP: (ha) => [/eqP ha1 ha2];move/andP: (hb) => [/eqP hb1 hb2]. have aa: a = a'. by move: (CF_bound ha) (CF_bound hb); rewrite -sv {4}ha1 {2}hb1 => <- ->. move:sv; rewrite aa /= => /addrI sv; congr cons. move: ha2 hb2 ss sv; clear;elim: l l'. case => // a l ha /andP[ea eb] hc /= ec. by move:(SCF_pos1 (all_rat_in_P_pos ea) isT); rewrite /= ec Order.POrderTheory.ltxx. move => a l Hrec; case; first by rewrite ltn0. move => a' l' /= /andP[/andP[pa pb] pc] /andP[/andP[qa qb] qc]. rewrite ltnS => ss. move /(congr1 (fun x => 1/x)); rewrite !div1r !invrK => ee'. have ll:(last 0 l != 1) by move: pc; case:(l). have ll':(last 0 l' != 1) by move: qc; case:(l'). have aa: a = a'. have g1: (good_for_cf a l). by rewrite /good_for_cf pb ll; move /andP: pa => [-> _]. have g2: (good_for_cf a' l'). by rewrite /good_for_cf qb ll'; move /andP: qa => [-> _]. move:(CF_bound g1) (CF_bound g2);rewrite /= ee' => <-. by move /andP: qa => [/eqP {3}-> _] ->; move /andP: pa => [/eqP <- _]. move: ee'; rewrite aa; move/addrI => ea. congr cons; apply: Hrec => //; [by rewrite pb ll | by rewrite qb ll']. 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)