- apply (exadecimal_of_nat_elim (λn.;
-
-
-
- elim n 0; [ reflexivity | intro ];
- elim n1 0; [ intros; reflexivity | intros 2 ];
- elim n2 0; [ intros; reflexivity | intros 2 ];
- elim n3 0; [ intros; reflexivity | intros 2 ];
- elim n4 0; [ intros; reflexivity | intros 2 ];
- elim n5 0; [ intros; reflexivity | intros 2 ];
- elim n6 0; [ intros; reflexivity | intros 2 ];
- elim n7 0; [ intros; reflexivity | intros 2 ];
- elim n8 0; [ intros; reflexivity | intros 2 ];
- elim n9 0; [ intros; reflexivity | intros 2 ];
- elim n10 0; [ intros; reflexivity | intros 2 ];
- elim n11 0; [ intros; reflexivity | intros 2 ];
- elim n12 0; [ intros; reflexivity | intros 2 ];
- elim n13 0; [ intros; reflexivity | intros 2 ];
- elim n14 0; [ intros; reflexivity | intros 2 ];
- elim n15 0; [ intros; reflexivity | intros 2 ];
+ rewrite > exadecimal_of_nat_mod;
+ generalize in match (lt_mod_m_m n 16 ?); [2: autobatch | ]
+ generalize in match (n \mod 16); intro;
+ cases n1; [ intro; reflexivity | ];
+ cases n2; [ intro; reflexivity | ];
+ cases n3; [ intro; reflexivity | ];
+ cases n4; [ intro; reflexivity | ];
+ cases n5; [ intro; reflexivity | ];
+ cases n6; [ intro; reflexivity | ];
+ cases n7; [ intro; reflexivity | ];
+ cases n8; [ intro; reflexivity | ];
+ cases n9; [ intro; reflexivity | ];
+ cases n10; [ intro; reflexivity | ];
+ cases n11 [ intro; reflexivity | ];
+ cases n12; [ intro; reflexivity | ];
+ cases n13; [ intro; reflexivity | ];
+ cases n14; [ intro; reflexivity | ];
+ cases n15; [ intro; reflexivity | ];
+ cases n16; [ intro; reflexivity | ];