proposition: Lemma Exercise5_9f n: natp n -> (Ex59_val \0c n) = Yo (n <=c \1c) \1c \0c.
proof: Proof. move => nN. move: (cleSltP NS1); rewrite succ_one => H. have cfN:=(NS_factorial nN); have cfn:= CS_nat cfN. rewrite /Ex59_val /Ex59_num /Ex59_den cprod0l factorial0 cpow1x (cprod1r cfn). case: (equal_or_not n \0c) => n0. by rewrite n0 factorial0 (cquo_one NS1) (Y_true (cle_01)). case: (equal_or_not n \1c) => n1. by rewrite n1 factorial1 (cquo_one NS1) (Y_true (cleR CS1)). have ln2:=(cge2 (CS_nat nN) n0 n1). move /H: (ln2) => /cltNge gn1. move:(factorial_monotone nN ln2); rewrite factorial2 => /H dg. by rewrite (cquo_small cfN dg) (Y_false gn1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)