proposition: Lemma CSB_comp2: forall y:Y, CSB_bijection (CSB_bijection2 y) = y.
proof: Proof. intro. unfold CSB_bijection2; case (classic_dec (Y_even y)). intro. unfold CSB_bijection; case (classic_dec (X_odd (g y))). intro. destruct ginv_odd. simpl. apply g_inj. assumption. intro. contradict n. constructor. assumption. intro. destruct finv_noteven. simpl. unfold CSB_bijection; case (classic_dec (X_odd x)). intro. contradict n. rewrite <- e. constructor 2. assumption. trivial. Qed.
imports: FunctionProperties DecidableDec Description Classical