proposition: Lemma as_Moebius_Q_L: forall x, Zero<x+3->as_Moebius_Q LL x= (x-1)/(x+3).
proof: Proof. intros x H_x; assert (H_x':x * 2 + 3 * 2 <> Zero); [stepl (2*(x+3)); auto; ring|]; unfold as_Moebius_Q, map_digits, fst, snd, Qdiv at 2 4; rewrite <- Qmult_assoc; rewrite Qmult_one_left; rewrite Qmult_sym; fold (Qdiv x 2); rewrite Qplus_Qdiv; auto; rewrite Qplus_Qdiv; auto; rewrite Qdiv_Qdiv_simplify; auto; qZ_numerals; field; auto. Qed.
imports: Streams Streams_addenda Raxioms