proposition: Lemma fix_gcd : forall x y, gcd x y = Gcd gcd x y.
proof: Proof. Proof using. applys~ (FixFun2_fix (measure2 plus)). unfold measure2. introv IH. unfolds. case_if~. case_if~. case_if. apply* IH. apply* IH. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat